Nuprl Lemma : invert-union_wf
11,40
postcript
pdf
A
,
B
:Type,
x
:(
A
+
B
). invert-union(
x
)
(
B
+
A
)
latex
ProofTree
Definitions
invert-union(
x
)
,
x
:
A
.
B
(
x
)
,
case
b
of inl(
x
) =>
s
(
x
) | inr(
y
) =>
t
(
y
)
,
inr
x
,
inl
x
,
left
+
right
,
t
T
,
Type
origin
A, B:Type, x:(A + B). invert-union(x) 
(B + A)
A, B:Type, x:(A + B). invert-union(x) (B + A)
x:A. B(x) T